package net.greyar.theory;

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

public class State {
	private int counter = 1;
	public static void main(String[] args) throws Exception {
		State.setDebug(true);
		List<Symbol> rules = Symbol.parseMany("" +
				"(equal ?x ?x)" +
				"(if (distinct ?x ?y) (not (equal ?x ?y)))" +
				"(if (next (control ?player)) (role ?player) (role ?other) (control ?other) (distinct ?player ?other))" +
				"(role o)" +
				"(role x)" +
				"(control x)" +
				"(if (legal ?player (mark ?x ?y)) (role ?player) (control ?player) (cell ?x ?y b))" +
				"(if (legal ?player noop) (role ?player) (role ?other) (control ?other) (distinct ?player ?other))" +
				"(cell 1 1 b)" +
				"(cell 1 2 x)" +
				"(cell 1 3 x)" +
				"(cell 2 1 o)" +
				"(cell 2 2 O)" +
				"(cell 2 3 b)" +
				"(cell 3 1 b)" +
				"(cell 3 2 o)" +
				"(cell 3 3 b)" +
				"(money 10)" +
				"(if (next (money ?x)) (money ?y) (equal ?x (neg ?y)))" +
				"");
		State state = new State(rules);
		Symbol query = Symbol.parse("(next ?x)");
		List<Substitution> next = state.find(query);
		System.err.println("Q:\t" + query);
		int i = 1;
		for (Substitution sigma : next) {
			System.err.println(i++ + ":\t" + query.apply(sigma) + "\t\t" + sigma);
		}
		System.err.println("-");
	}
	private static boolean debug = false;
	private int level = 0;
	private String tab = "    ";
	private Map<String, List<Symbol>> rules;
	private Map<String, List<Symbol>> facts;
	public State(List<Symbol> rules) {
		this.rules = loadRules(rules);
		this.facts = Collections.synchronizedMap(new HashMap<String, List<Symbol>>());
	}
	private Map<String, List<Symbol>> loadRules(List<Symbol> rules) {
		Map<String, List<Symbol>> map = new HashMap<String, List<Symbol>>();
		for (Symbol rule : rules) {
			if (!map.containsKey(rule.getKey())) {
				map.put(rule.getKey(), new ArrayList<Symbol>());
			}
			map.get(rule.getKey()).add(rule);
		}
		return Collections.unmodifiableMap(map);
	}
	public void addFact(Symbol fact) {
		synchronized (facts) {
			if (!facts.containsKey(fact.getKey())) {
				facts.put(fact.getKey(), new ArrayList<Symbol>());
			}
			facts.get(fact.getKey()).add(fact);
		}
	}
	public void addFacts(List<Symbol> list) {
		synchronized (facts) {
			for (Symbol fact : list) {
				if (!facts.containsKey(fact.getKey())) {
					facts.put(fact.getKey(), new ArrayList<Symbol>());
				}
				facts.get(fact.getKey()).add(fact);
			}
		}
	}
	public void clear() {
		synchronized (facts) {
			facts.clear();
		}
	}
	private List<Symbol> getFacts(Symbol query) {
		List<Symbol> results = new ArrayList<Symbol>();
		if (query instanceof Variable) {
			for (List<Symbol> symbols : rules.values()) {
				results.addAll(symbols);
			}
			for (List<Symbol> symbols : facts.values()) {
				results.addAll(symbols);
			}
		} else if (query.getKey().indexOf('?') == 0) {
			for (String key : rules.keySet()) {
				for (Symbol symbol : rules.get(key)) {
					if (symbol instanceof Rule) {
						if (symbol.get(1).size() == query.size()) {
							results.add(symbol);
						}
					} else {
						if (symbol.size() == query.size()) {
							results.add(symbol);
						}
					}
				}
			}
			for (String key : facts.keySet()) {
				for (Symbol symbol : facts.get(key)) {
					if (symbol instanceof Rule) {
						if (symbol.get(1).size() == query.size()) {
							results.add(symbol);
						}
					} else {
						if (symbol.size() == query.size()) {
							results.add(symbol);
						}
					}
				}
			}
		} else {
			if (rules.containsKey(query.getKey())) {
				for (Symbol symbol : rules.get(query.getKey())) {
					results.add(symbol.apply(new Substitution()));
				}
			}
			if (facts.containsKey(query.getKey())) {
				for (Symbol symbol : facts.get(query.getKey())) {
					results.add(symbol.apply(new Substitution()));
				}
			}
		}
		debug(": facts " + results);
		return results;
	}
	public List<Substitution> find(Symbol query) {
		level = 0;
		debug(level + " find " + query);
		level++;
		return find(query, new Substitution());
	}
	public List<Symbol> results(Symbol query) {
		List<Symbol> results = new ArrayList<Symbol>();
		for (Substitution found : find(query)) {
			results.add(query.apply(found, new HashMap<String, Variable>()));
		}
		return results;
	}
	private List<Substitution> find(Symbol query, Substitution sigma) {
		if (query instanceof Variable) {
			query = sigma.last(query);
		}
		if (query instanceof Rule) {
			return rule(query, sigma);
		}
		if (query instanceof Not) {
			return not(query, sigma);
		}
		if (query instanceof Equal) {
			return equal(query, sigma);
		}
		if (query instanceof Distinct) {
			return distinct(query, sigma);
		}
		if (query instanceof And) {
			return and(query, sigma);
		}
		if (query instanceof Or) {
			return or(query, sigma);
		}
		if (query instanceof Sum) {
			return sum(query, sigma);
		}
		if (query instanceof Multiplication) {
			return mult(query, sigma);
		}
		if (query instanceof Negative) {
			return neg(query, sigma);
		}
		if (query instanceof Absolute) {
			return abs(query, sigma);
		}
		List<Substitution> found = new ArrayList<Substitution>();
		for (Symbol fact : getFacts(query)) {
			if (fact instanceof Rule) {
				Substitution result = query.unify(fact.get(1), sigma.copy());
				debug((result == null ? "" : "* ") + "head " + fact.get(1) + " ... " + result);
				if (result != null) {
					debug("+ premises " + fact.getSymbols().subList(2, fact.size()));
					List<Substitution> candidates = new ArrayList<Substitution>();
					candidates.add(result);
					for (int i = 2; i < fact.size(); i++) {
						debug((i - 1) + " find " + fact.get(i) + " " + candidates);
						level++;
						int height = candidates.size();
						for (int j = 0; j < height; j++) {
							debug((j + 1) + " " + candidates.get(0));
							level++;
							candidates.addAll(find(fact.get(i), candidates.remove(0)));
							level--;
							debug("| candidates " + candidates);
						}
						level--;
					}
					found.addAll(candidates);
				}
			} else {
				Substitution result = query.unify(fact, sigma.copy());
				debug((result == null ? "" : "* ") + "fact " + fact + " ... " + result);
				if (result != null) {
					found.add(result);
				}
			}
		}
		debug("| found " + found, -1);
		return found;
	}
	private List<Substitution> abs(Symbol query, Substitution sigma) {
		debug("! abs");
		List<Substitution> found = new ArrayList<Substitution>();
		if (query.grounds(sigma)) {
			debug("_ grounds");
			debug(". find " + query.apply(sigma));
			level++;
			found = find(query.apply(sigma), sigma);
			level--;
		} else {
			found.add(sigma);
		}
		debug(". found ... " + found, -1);
		return found;
	}
	private List<Substitution> neg(Symbol query, Substitution sigma) {
		debug("! neg");
		List<Substitution> found = new ArrayList<Substitution>();
		if (query.grounds(sigma)) {
			debug("_ grounds");
			debug("- find " + query.apply(sigma));
			level++;
			found = find(query.apply(sigma), sigma);
			level--;
		} else {
			found.add(sigma);
		}
		debug("- found ... " + found, -1);
		return found;
	}
	private List<Substitution> mult(Symbol query, Substitution sigma) {
		debug("! mult");
		List<Substitution> found = new ArrayList<Substitution>();
		if (query.grounds(sigma)) {
			debug("_ grounds");
			debug("x find " + query.apply(sigma));
			level++;
			found = find(query.apply(sigma), sigma);
			level--;
		} else {
			found.add(sigma);
		}
		debug("x found ... " + found, -1);
		return found;
	}
	private List<Substitution> sum(Symbol query, Substitution sigma) {
		debug("! sum");
		List<Substitution> found = new ArrayList<Substitution>();
		if (query.grounds(sigma)) {
			debug("_ grounds");
			debug("+ find " + query.apply(sigma));
			level++;
			found = find(query.apply(sigma), sigma);
			level--;
		} else {
			found.add(sigma);
		}
		debug("+ found ... " + found, -1);
		return found;
	}
	private List<Substitution> and(Symbol query, Substitution sigma) {
		debug("! and");
		List<Substitution> found = new ArrayList<Substitution>();
		debug("+ terms " + query.getSymbols().subList(1, query.size()));
		for (int i = 1; i < query.size(); i++) {
			debug(i + " find " + query.get(i));
			level++;
			int height = found.size();
			for (int j = 0; j < height; j++) {
				debug(j + " find " + found.get(0));
				level++;
				found.addAll(find(query.get(i), found.remove(0)));
				level--;
				debug("| candidates " + found);
			}
			level--;
		}
		debug(". found " + found, -1);
		return found;
	}
	private List<Substitution> or(Symbol query, Substitution sigma) {
		debug("! or");
		List<Substitution> found = new ArrayList<Substitution>();
		debug("+ terms " + query.getSymbols().subList(1, query.size()));
		for (int i = 1; i < query.size(); i++) {
			debug(i + " find " + query.get(i) + " " + found.get(0));
			level++;
			found.addAll(find(query.get(i), found.remove(0)));
			level--;
			debug("| candidates " + found);
		}
		debug(". found " + found, -1);
		return found;
	}
	private List<Substitution> rule(Symbol query, Substitution sigma) {
		debug("! rule");
		debug("| find " + query.get(1) + " " + sigma);
		level++;
		List<Substitution> found = find(query.get(1), sigma);
		level--;
		debug("| premises " + query.getSymbols().subList(2, query.size()));
		for (int i = 2; i < query.size(); i++) {
			int height = found.size();
			for (int j = 0; j < height; j++) {
				debug((i - 1) + " find " + query.get(i) + " " + found.get(0));
				level++;
				found.addAll(find(query.get(i), found.remove(0)));
				level--;
				debug(": found " + found);
			}
		}
		debug(". found " + found, -1);
		return found;
	}
	private List<Substitution> equal(Symbol query, Substitution sigma) {
		debug("! equal");
		if (query.grounds(sigma)) {
			List<Substitution> found = new ArrayList<Substitution>();
			debug("_ grounds");
			for (int i = 1; i < query.size() - 1; i++) {
				sigma = query.get(i).unify(query.get(i+ 1), sigma);
				debug((sigma == null ? "" : "* ") + query.get(i) + " == " + query.get(i+ 1) + " ... " + sigma);
				if (sigma == null) {
					debug("~ not equal ... " + found, -1);
					return found;
				}
			}
			found.add(sigma);
			debug("= found ... " + found, -1);
			return found;
		} else {
			for (int i = 1; i < query.size() - 1; i++) {
				debug("# constrain " + query.get(i) + " :: " + query.get(i + 1));
				sigma.constrain(query.get(i), query.get(i + 1));
			}
			Symbol and = new And(query.getSymbols().subList(1, query.size()));
			debug("= find " + and + " " + sigma);
			level++;
			List<Substitution> found = find(and, sigma);
			level--;
			if (found.isEmpty()) {
				found.add(sigma);
			}
			debug("= found ... " + found, -1);
			return found;
		}
	}
	private List<Substitution> distinct(Symbol query, Substitution sigma) {
		debug("! distinct");
		if (query.grounds(sigma)) {
			List<Substitution> found = new ArrayList<Substitution>();
			debug("_ grounds");
			for (int i = 1; i < query.size() - 1; i++) {
				for (int j = i + 1; j < query.size(); j++) {
					Substitution copy = query.get(i).unify(query.get(j), sigma.copy());
					debug((copy == null ? "* " : "") + query.get(i) + " != " + query.get(i+ 1) + " ... " + copy);
					if (copy != null) {
						debug("= not distinct ... " + found, -1);
						return found;
					}
				}
			}
			found.add(sigma);
			debug("~ found ... " + found, -1);
			return found;
		} else {
			for (int i = 1; i < query.size() - 1; i++) {
				for (int j = i + 1; j < query.size(); j++) {
					debug("# constrain " + query.get(i) + " :: " + new Not(query.get(j)));
					sigma.constrain(query.get(i), query.get(j));
				}
			}
			Symbol or = new Or(query.getSymbols().subList(1, query.size()));
			debug("~ find " + or + " " + sigma);
			level++;
			List<Substitution> found = find(or, sigma);
			level--;
			if (found.isEmpty()) {
				found.add(sigma);
			}
			debug("~ found ... " + found, -1);
			return found;
		}
	}
	private List<Substitution> not(Symbol query, Substitution sigma) {
		debug("! not");
		debug("| find " + query.get(1) + " " + sigma);
		level++;
		List<Substitution> found = find(query.get(1), sigma);
		level--;
		if (found.size() > 0) {
			found.clear();
		} else {
			found.add(sigma);
		}
		debug("\u00A6 found ... " + found, -1);
		return found;
	}
	public List<Symbol> getRules() {
		List<Symbol> result = new ArrayList<Symbol>();
		for (List<Symbol> list : rules.values()) {
			result.addAll(list);
		}
		return Collections.unmodifiableList(result);
	}
	private void debug(String line) {
		if (debug) {
			System.out.print(counter++ + "\t");
			for (int i = 0; i < level; i++) {
				System.out.print(tab);
			}
			System.out.println(line);
		}
	}
	private void debug(String line, int indentOffset) {
		if (debug) {
			System.out.print(counter++ + "\t");
			for (int i = 0; i < level + indentOffset; i++) {
				System.out.print(tab);
			}
			System.out.println(line);
		}
	}
	public static boolean isDebug() {
		return debug;
	}
	public static void setDebug(boolean debug) {
		State.debug = debug;
	}
}
